Extensional higher-order logic programming has been introduced as ageneralization of classical logic programming. An important characteristic ofthis paradigm is that it preserves all the well-known properties of traditionallogic programming. In this paper we consider the semantics of negation in thecontext of the new paradigm. Using some recent results from non-monotonicfixed-point theory, we demonstrate that every higher-order logic program withnegation has a unique minimum infinite-valued model. In this way we obtain thefirst purely model-theoretic semantics for negation in extensional higher-orderlogic programming. Using our approach, we resolve an old paradox that wasintroduced by W. W. Wadge in order to demonstrate the semantic difficulties ofhigher-order logic programming.
展开▼
机译:扩展高阶逻辑编程已作为经典逻辑编程的一般化引入。该范例的一个重要特征是它保留了传统逻辑编程的所有众所周知的属性。在本文中,我们在新范式的背景下考虑了否定的语义。使用非单调不动点理论的一些最新结果,我们证明了每个带负数的高阶逻辑程序都有一个唯一的最小无穷大模型。通过这种方式,我们获得了扩展高阶逻辑编程中否定的第一个纯模型理论语义。使用我们的方法,我们解决了W. W. Wadge引入的一个古老的悖论,以证明高阶逻辑编程的语义困难。
展开▼